Termination Proof Script

Consider the TRS R consisting of the rewrite rule
1:    app(app(iterate,f),x)  → app(app(cons,x),app(app(iterate,f),app(f,x)))
There are 4 dependency pairs:
2:    APP(app(iterate,f),x)  → APP(app(cons,x),app(app(iterate,f),app(f,x)))
3:    APP(app(iterate,f),x)  → APP(cons,x)
4:    APP(app(iterate,f),x)  → APP(app(iterate,f),app(f,x))
5:    APP(app(iterate,f),x)  → APP(f,x)
The approximated dependency graph contains one SCC: {2,4,5}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 3, 2006